SherbyNet - /page/wikibook/entry.mu

<!DOCTYPE html>

<title>Simulation (computer science)</title>

</head>

Simulation (computer science)

</h1>

</header>

<div id="mw-content-text" class="mw-body-content mw-content-ltr" lang="en" dir="ltr"><div class="mw-content-ltr mw-parser-output" lang="en" dir="ltr">In <a href="Theoretical_computer_science" title="Theoretical computer science">theoretical computer science</a> a simulation is a <a href="Relation_(mathematics)" title="Relation (mathematics)">relation</a> between <a href="State_transition_system" class="mw-redirect" title="State transition system">state transition systems</a> associating systems that behave in the same way in the sense that one system simulates the other.

Intuitively, a system simulates another system if it can match all of its moves.

The basic definition relates states within one transition system, but this is easily adapted to relate two separate transition systems by building a system consisting of the <a href="Disjoint_union" title="Disjoint union">disjoint union</a> of the corresponding components.

<div class="mw-heading mw-heading2"><h2 id="Formal_definition">Formal definition</h2></div>

Given a <a href="State_transition_system" class="mw-redirect" title="State transition system">labelled state transition system</a> (<math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle S}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle S}</annotation>

</semantics>

</math><img src="./4611d85173cd3b508e67077d4a1252c9c05abca2.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.499ex; height:2.176ex;" alt="{\displaystyle S}" loading="lazy">, <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \Lambda }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \Lambda }</annotation>

</semantics>

</math><img src="./0ac0a4a98a414e3480335f9ba652d12571ec6733.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.613ex; height:2.176ex;" alt="{\displaystyle \Lambda }" loading="lazy">, →),

where <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle S}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle S}</annotation>

</semantics>

</math><img src="./4611d85173cd3b508e67077d4a1252c9c05abca2.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.499ex; height:2.176ex;" alt="{\displaystyle S}" loading="lazy"> is a set of states, <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \Lambda }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \Lambda }</annotation>

</semantics>

</math><img src="./0ac0a4a98a414e3480335f9ba652d12571ec6733.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.613ex; height:2.176ex;" alt="{\displaystyle \Lambda }" loading="lazy"> is a set of labels and → is a set of labelled transitions (i.e., a subset of <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle S\times \Lambda \times S}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle S\times \Lambda \times S}</annotation>

</semantics>

</math><img src="./b33e37ce4a542e2949580c19ff9e01283fedd285.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:10.292ex; height:2.176ex;" alt="{\displaystyle S\times \Lambda \times S}" loading="lazy">),

a relation <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle R\subseteq S\times S}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle R\subseteq S\times S}</annotation>

</semantics>

</math><img src="./4957f9171a9ea27d56e924189350b5468f67579e.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.505ex; width:10.701ex; height:2.343ex;" alt="{\displaystyle R\subseteq S\times S}" loading="lazy"> is a simulation if and only if for every pair of states <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle (p,q)}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle (p,q)}</annotation>

</semantics>

</math><img src="./9769c58523b9b639866a2d48e657d9c26911143a.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:5.082ex; height:2.843ex;" alt="{\displaystyle (p,q)}" loading="lazy"> in <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle R}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle R}</annotation>

</semantics>

</math><img src="./4b0bfb3769bf24d80e15374dc37b0441e2616e33.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.764ex; height:2.176ex;" alt="{\displaystyle R}" loading="lazy"> and all labels λ in <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \Lambda }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \Lambda }</annotation>

</semantics>

</math><img src="./0ac0a4a98a414e3480335f9ba652d12571ec6733.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.613ex; height:2.176ex;" alt="{\displaystyle \Lambda }" loading="lazy">:

<mover>

</mover>

</mrow>

<msup>

</msup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle p{\overset {\lambda }{\rightarrow }}p'}</annotation>

</semantics>

</math><img src="./888c14a7d1db7237c4095dd0766a5579771e3968.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; margin-left: -0.089ex; width:5.437ex; height:4.009ex;" alt="{\displaystyle p{\overset {\lambda }{\rightarrow }}p'}" loading="lazy">, then there is <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle q{\overset {\lambda }{\rightarrow }}q'}">

<mover>

</mover>

</mrow>

<msup>

</msup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle q{\overset {\lambda }{\rightarrow }}q'}</annotation>

</semantics>

</math><img src="./92accb67a0e7c5f20ff7c1d2acfe5127bf33f669.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:5.157ex; height:4.009ex;" alt="{\displaystyle q{\overset {\lambda }{\rightarrow }}q'}" loading="lazy"> such that <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle (p',q')\in R}">

<msup>

</msup>

<msup>

</msup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle (p',q')\in R}</annotation>

</semantics>

</math><img src="./42f2387df3f3a1b61f2e1052169e7e02095ed442.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:11.066ex; height:3.009ex;" alt="{\displaystyle (p',q')\in R}" loading="lazy"></dd></dl>

Equivalently, in terms of <a href="Composition_of_relations" title="Composition of relations">relational composition</a>:

<msup>

</mrow>

</msup>

<mover>

</mover>

</mrow>

</mrow>

<mover>

</mover>

</mrow>

<msup>

</mrow>

</msup>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle R^{-1}\,;\,{\overset {\lambda }{\rightarrow }}\quad {\subseteq }\quad {\overset {\lambda }{\rightarrow }}\,;\,R^{-1}}</annotation>

</semantics>

</math><img src="./42d8df8d3378dfc924f459f50acefb5cf2f07ad8.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:22.911ex; height:4.009ex;" alt="{\displaystyle R^{-1}\,;\,{\overset {\lambda }{\rightarrow }}\quad {\subseteq }\quad {\overset {\lambda }{\rightarrow }}\,;\,R^{-1}}" loading="lazy"></dd></dl>

Given two states <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle p}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle p}</annotation>

</semantics>

</math><img src="./81eac1e205430d1f40810df36a0edffdc367af36.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; margin-left: -0.089ex; width:1.259ex; height:2.009ex;" alt="{\displaystyle p}" loading="lazy"> and <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle q}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle q}</annotation>

</semantics>

</math><img src="./06809d64fa7c817ffc7e323f85997f783dbdf71d.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.07ex; height:2.009ex;" alt="{\displaystyle q}" loading="lazy"> in <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle S}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle S}</annotation>

</semantics>

</math><img src="./4611d85173cd3b508e67077d4a1252c9c05abca2.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.499ex; height:2.176ex;" alt="{\displaystyle S}" loading="lazy">, <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle p}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle p}</annotation>

</semantics>

</math><img src="./81eac1e205430d1f40810df36a0edffdc367af36.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; margin-left: -0.089ex; width:1.259ex; height:2.009ex;" alt="{\displaystyle p}" loading="lazy"> can be simulated by <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle q}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle q}</annotation>

</semantics>

</math><img src="./06809d64fa7c817ffc7e323f85997f783dbdf71d.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.07ex; height:2.009ex;" alt="{\displaystyle q}" loading="lazy">, written <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle p\,\leq \,q}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle p\,\leq \,q}</annotation>

</semantics>

</math><img src="./d2656dcd48cf31f34a9bca41d2c80b0aa2444b59.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; margin-left: -0.089ex; width:6.201ex; height:2.343ex;" alt="{\displaystyle p\,\leq \,q}" loading="lazy">, if and only if there is a simulation <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle R}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle R}</annotation>

</semantics>

</math><img src="./4b0bfb3769bf24d80e15374dc37b0441e2616e33.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.764ex; height:2.176ex;" alt="{\displaystyle R}" loading="lazy"> such that <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle (p,q)\in R}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle (p,q)\in R}</annotation>

</semantics>

</math><img src="./68416fab89bda4c6db561425a7f38d00a2ef8b6f.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:9.687ex; height:2.843ex;" alt="{\displaystyle (p,q)\in R}" loading="lazy">. The relation <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \leq }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \leq }</annotation>

</semantics>

</math><img src="./440568a09c3bfdf0e1278bfa79eb137c04e94035.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.505ex; width:1.808ex; height:2.176ex;" alt="{\displaystyle \leq }" loading="lazy"> is called the simulation preorder, and it is the union of all simulations: <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle (p,q)\in \,\leq \,}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle (p,q)\in \,\leq \,}</annotation>

</semantics>

</math><img src="./70a9d1b241b475d433f557b02a88ac4e08804673.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:9.86ex; height:2.843ex;" alt="{\displaystyle (p,q)\in \,\leq \,}" loading="lazy"> precisely when <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle (p,q)\in R}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle (p,q)\in R}</annotation>

</semantics>

</math><img src="./68416fab89bda4c6db561425a7f38d00a2ef8b6f.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:9.687ex; height:2.843ex;" alt="{\displaystyle (p,q)\in R}" loading="lazy"> for some simulation <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle R}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle R}</annotation>

</semantics>

</math><img src="./4b0bfb3769bf24d80e15374dc37b0441e2616e33.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.764ex; height:2.176ex;" alt="{\displaystyle R}" loading="lazy">.

The set of simulations is closed under union;<a href="#cite_note-1">[Note 1]</a> therefore, the simulation preorder is itself a simulation. Since it is the union of all simulations, it is the unique largest simulation. Simulations are also closed under <a href="Reflexive_closure" title="Reflexive closure">reflexive</a> and <a href="Transitive_closure" title="Transitive closure">transitive</a> closure; therefore, the largest simulation must be reflexive and transitive. From this follows that the largest simulation—the simulation preorder—is indeed a <a href="Preorder" title="Preorder">preorder relation</a>.<a href="#cite_note-2">[1]</a> Note that there can be more than one relation that is both a simulation and a preorder;<a href="#cite_note-3">[Note 2]</a> the term simulation preorder refers to the largest one of them (which is a superset of all the others).

Two states <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle p}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle p}</annotation>

</semantics>

</math><img src="./81eac1e205430d1f40810df36a0edffdc367af36.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; margin-left: -0.089ex; width:1.259ex; height:2.009ex;" alt="{\displaystyle p}" loading="lazy"> and <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle q}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle q}</annotation>

</semantics>

</math><img src="./06809d64fa7c817ffc7e323f85997f783dbdf71d.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.07ex; height:2.009ex;" alt="{\displaystyle q}" loading="lazy"> are said to be similar, written <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle p\leq \geq q}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle p\leq \geq q}</annotation>

</semantics>

</math><img src="./45f7e895e642e5b3d613f240d9d32565c3559e02.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; margin-left: -0.089ex; width:7.235ex; height:2.343ex;" alt="{\displaystyle p\leq \geq q}" loading="lazy">, if and only if <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle p}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle p}</annotation>

</semantics>

</math><img src="./81eac1e205430d1f40810df36a0edffdc367af36.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; margin-left: -0.089ex; width:1.259ex; height:2.009ex;" alt="{\displaystyle p}" loading="lazy"> can be simulated by <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle q}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle q}</annotation>

</semantics>

</math><img src="./06809d64fa7c817ffc7e323f85997f783dbdf71d.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.07ex; height:2.009ex;" alt="{\displaystyle q}" loading="lazy"> and <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle q}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle q}</annotation>

</semantics>

</math><img src="./06809d64fa7c817ffc7e323f85997f783dbdf71d.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.07ex; height:2.009ex;" alt="{\displaystyle q}" loading="lazy"> can be simulated by <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle p}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle p}</annotation>

</semantics>

</math><img src="./81eac1e205430d1f40810df36a0edffdc367af36.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; margin-left: -0.089ex; width:1.259ex; height:2.009ex;" alt="{\displaystyle p}" loading="lazy">. Similarity is thus the maximal symmetric subset of the simulation preorder, which means it is reflexive, symmetric, and transitive; hence an <a href="Equivalence_relation" title="Equivalence relation">equivalence relation</a>. However, it is not necessarily a simulation, and precisely in those cases when it is not a simulation, it is strictly coarser than <a href="Bisimilarity" class="mw-redirect" title="Bisimilarity">bisimilarity</a> (meaning it is a superset of bisimilarity).<a href="#cite_note-4">[Note 3]</a>

To witness, consider a similarity that is a simulation. Since it is symmetric, it is a bisimulation. It must then be a subset of bisimilarity, which is the union of all bisimulations. Yet it is easy to see that similarity is always a superset of bisimilarity. From this follows that if similarity is a simulation, it equals bisimilarity. And if it equals bisimilarity, it is naturally a simulation (since bisimilarity is a simulation). Therefore, similarity is a simulation if and only if it equals bisimilarity. If it does not, it must be its strict superset; hence a strictly coarser equivalence relation.

<div class="mw-heading mw-heading2"><h2 id="Similarity_of_separate_transition_systems">Similarity of separate transition systems</h2></div>

When comparing two different transition systems (S', Λ', →') and (S", Λ", →"), the basic notions of simulation and similarity can be used by forming the disjoint composition of the two machines, (S, Λ, →) with S = S' ∐ S", Λ = Λ' ∪ Λ" and → = →' ∪ →", where ∐ is the <a href="Disjoint_union" title="Disjoint union">disjoint union</a> operator between sets.

<ul><li><a href="State_transition_system" class="mw-redirect" title="State transition system">State transition system</a></li>

<li><a href="Bisimulation" title="Bisimulation">Bisimulation</a></li>

<li><a href="Coinduction" title="Coinduction">Coinduction</a></li>

<li><a href="Operational_semantics" title="Operational semantics">Operational semantics</a></li></ul>

<div class="mw-heading mw-heading2"><h2 id="Notes">Notes</h2></div>

/* start https://en.wikipedia.org/ */

.mw-parser-output .reflist{margin-bottom:0.5em;list-style-type:decimal}@media screen{.mw-parser-output .reflist{font-size:90%}}.mw-parser-output .reflist .references{font-size:100%;margin-bottom:0;list-style-type:inherit}.mw-parser-output .reflist-columns-2{column-width:30em}.mw-parser-output .reflist-columns-3{column-width:25em}.mw-parser-output .reflist-columns{margin-top:0.3em}.mw-parser-output .reflist-columns ol{margin-top:0}.mw-parser-output .reflist-columns li{page-break-inside:avoid;break-inside:avoid-column}.mw-parser-output .reflist-upper-alpha{list-style-type:upper-alpha}.mw-parser-output .reflist-upper-roman{list-style-type:upper-roman}.mw-parser-output .reflist-lower-alpha{list-style-type:lower-alpha}.mw-parser-output .reflist-lower-greek{list-style-type:lower-greek}.mw-parser-output .reflist-lower-roman{list-style-type:lower-roman}

/* end https://en.wikipedia.org/ */

</style><div class="reflist">

Meaning the union of two simulations is a simulation.

</li>

<li id="cite_note-3"><a href="#cite_ref-3">^</a> Consider the relations <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \{\}}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \{\}}</annotation>

</semantics>

</math><img src="./3e6f1caa524dfcc90158ad69a51b5f9577fe5f1f.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:2.325ex; height:2.843ex;" alt="{\displaystyle \{\}}" loading="lazy"> and <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \{(0,0)\}}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \{(0,0)\}}</annotation>

</semantics>

</math><img src="./4cbad44c2d005cef02704bc348a361e5b664593e.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:7.493ex; height:2.843ex;" alt="{\displaystyle \{(0,0)\}}" loading="lazy">—each is both a simulation and a preorder.

</li>

<li id="cite_note-4"><a href="#cite_ref-4">^</a> For an example, see Fig. 1 in <style data-mw-deduplicate="TemplateStyles:r1238218222">

/* start https://en.wikipedia.org/ */

.mw-parser-output cite.citation{font-style:inherit;word-wrap:break-word}.mw-parser-output .citation q{quotes:"\"""\"""'""'"}.mw-parser-output .citation:target{background-color:rgba(0,127,255,0.133)}.mw-parser-output .id-lock-free.id-lock-free a{background:url("./mw/Lock-green.svg")right 0.1em center/9px no-repeat}.mw-parser-output .id-lock-limited.id-lock-limited a,.mw-parser-output .id-lock-registration.id-lock-registration a{background:url("./mw/Lock-gray-alt-2.svg")right 0.1em center/9px no-repeat}.mw-parser-output .id-lock-subscription.id-lock-subscription a{background:url("./mw/Lock-red-alt-2.svg")right 0.1em center/9px no-repeat}.mw-parser-output .cs1-ws-icon a{background:url("./mw/Wikisource-logo.svg")right 0.1em center/12px no-repeat}body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-free a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-limited a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-registration a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-subscription a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .cs1-ws-icon a{background-size:contain;padding:0 1em 0 0}.mw-parser-output .cs1-code{color:inherit;background:inherit;border:none;padding:inherit}.mw-parser-output .cs1-hidden-error{display:none;color:var(--color-error,#d33)}.mw-parser-output .cs1-visible-error{color:var(--color-error,#d33)}.mw-parser-output .cs1-maint{display:none;color:#085;margin-left:0.3em}.mw-parser-output .cs1-kern-left{padding-left:0.2em}.mw-parser-output .cs1-kern-right{padding-right:0.2em}.mw-parser-output .citation .mw-selflink{font-weight:inherit}@media screen{.mw-parser-output .cs1-format{font-size:95%}html.skin-theme-clientpref-night .mw-parser-output .cs1-maint{color:#18911f}}@media screen and (prefers-color-scheme:dark){html.skin-theme-clientpref-os .mw-parser-output .cs1-maint{color:#18911f}}

/* end https://en.wikipedia.org/ */

</style><cite id="CITEREFChamparnaudCoulon2004" class="citation journal cs1">Champarnaud, J.-M; Coulon, F. (2004). <a rel="nofollow" class="external text" href="https://doi.org/10.1016%2Fj.tcs.2004.02.048">"NFA reduction algorithms by means of regular inequalities"</a>. <a href="Theoretical_Computer_Science_(journal)" title="Theoretical Computer Science (journal)">Theoretical Computer Science</a>. 327 (3): 241–253. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1016%2Fj.tcs.2004.02.048">10.1016/j.tcs.2004.02.048</a>. <a href="ISSN_(identifier)" class="mw-redirect" title="ISSN (identifier)">ISSN</a> <a rel="nofollow" class="external text" href="https://search.worldcat.org/issn/0304-3975">0304-3975</a>.</cite>

</li>

</ol></div></div>

<div class="mw-heading mw-heading2"><h2 id="References">References</h2></div>

<ol><li><cite id="CITEREFPark1981" class="citation conference cs1">Park, David (1981). <a rel="nofollow" class="external text" href="http://wrap.warwick.ac.uk/47224/1/WRAP_Park_cs-rr-035.pdf">"Concurrency and Automata on Infinite Sequences"</a> (PDF). In Deussen, Peter (ed.). Proceedings of the 5th GI-Conference, Karlsruhe. <a href="Lecture_Notes_in_Computer_Science" title="Lecture Notes in Computer Science">Lecture Notes in Computer Science</a>. Vol. 104. <a href="Springer-Verlag" class="mw-redirect" title="Springer-Verlag">Springer-Verlag</a>. pp. 167–183. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1007%2FBFb0017309">10.1007/BFb0017309</a>. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>978-3-540-10576-3</bdi>.</cite></li>

<li><cite id="CITEREFvan_Glabbeek2001" class="citation conference cs1">van Glabbeek, R. J. (2001). "The Linear Time – Branching Time Spectrum I: The Semantics of Concrete, Sequential Processes". Handbook of Process Algebra. Elsevier. pp. 3–99.</cite></li></ol>

<li id="cite_note-2"><a href="#cite_ref-2">^</a> <cite id="CITEREFMilner1989" class="citation book cs1"><a href="Robin_Milner" title="Robin Milner">Milner, Robin</a> (1989). Communication and Concurrency. USA: Prentice-Hall, Inc. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>0131149849</bdi>.</cite>

</li>

</ol></div></div><div><div class="zim-footer">

This article is issued from <a class="external text" title="Last edited on 2024-03-20" href="https://en.wikipedia.org/wiki/?title=Simulation_(computer_science)&oldid=1214680650">Wikipedia</a>. The text is available under <a class="external text" href="https://creativecommons.org/licenses/by-sa/4.0/deed.en">Creative Commons Attribution-Share Alike 4.0</a> unless otherwise noted. Additional terms may apply for the media files.

</div>

</div></div>

</div>

</main>

</div>

</body></html>